Step of Proof: bool_sim_true
12,41
postcript
pdf
Inference at
*
1
I
of proof for Lemma
bool
sim
true
:
1.
b
:
2.
b
= tt
b
~ tt
latex
by MemCD
latex
1
:
1:
b
= tt
.
Definitions
t
T
,
{
T
}
,
P
Q
,
x
:
A
.
B
(
x
)
,
SQType(
T
)
Lemmas
bool
sq
origin
b ~ tt
by MemCD
1:
1: b = tt
.
b ~ tt
by MemCD
1:
1: b = tt
.
T
Q
x:A. B(x)